\begin{tabbing}
R{-}FeasibleWitness\=\{i:l\}\+
\\[0ex]($R$; ${\it sv}$; ${\it av}$; ${\it dis}$; ${\it cl}$; ${\it fr}$; ${\it sfr}$; ${\it rfr}$; ${\it afr}$; ${\it bfr}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $R$ of \+
\\[0ex]Rnone =$>$ Rnone() = Rnone()
\\[0ex]Rplus(${\it left}$,${\it right}$)=$>$${\it rec}_{1}$,${\it rec}_{2}$.${\it rec}_{1}$ \& ${\it rec}_{2}$
\\[0ex]Rinit(${\it loc}$,$T$,$x$,$v$)=$>$ ${\it cl}$(${\it loc}$,$<$1, $x$$>$) = Rinit(${\it loc}$;$T$;$x$;$v$)
\\[0ex]\& ${\it sv}$($x$) = $<$$T$, $v$$>$
\\[0ex]\& ${\it dis}$(${\it loc}$,$x$) = isl($v$)
\\[0ex]Rframe(${\it loc}$,$T$,$x$,$L$)=$>$ ${\it cl}$(${\it loc}$,$<$2, $x$$>$) = Rframe(${\it loc}$;$T$;$x$;$L$)
\\[0ex]\& ((${\it sv}$($x$)).1) = $T$
\\[0ex]\& ${\it fr}$(${\it loc}$,$x$) = $L$
\\[0ex]Rsframe(${\it lnk}$,${\it tag}$,$L$)=$>$ ${\it cl}$(source(${\it lnk}$),$<$3, ${\it lnk}$, ${\it tag}$$>$) = Rsframe(${\it lnk}$;${\it tag}$;$L$)
\\[0ex]\& ${\it sfr}$(${\it lnk}$,${\it tag}$) = $L$
\\[0ex]Reffect(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$)=$>$ ${\it cl}$(${\it loc}$,$<$4, ${\it knd}$, $x$$>$) = Reffect(${\it loc}$;${\it ds}$;${\it knd}$;$T$;$x$;$f$)
\\[0ex]\& isl($f$) = isl((${\it sv}$($x$)).2)
\\[0ex]\& $\forall$$z$$\in$dom(${\it ds}$). $A$=${\it ds}$($z$) $\Rightarrow$  ((${\it sv}$($z$)).1) = $A$ \& ${\it av}$(${\it knd}$) = $T$
\\[0ex]\& (($\uparrow$isrcv(${\it knd}$)) $\Rightarrow$ (${\it loc}$ = destination(lnk(${\it knd}$))))
\\[0ex]\& (${\it knd}$ $\in$ ${\it fr}$(${\it loc}$,$x$))
\\[0ex]\& ($\forall$$z$$\in$fpf{-}domain(${\it ds}$). (${\it knd}$ $\in$ ${\it rfr}$(${\it loc}$,$z$)))
\\[0ex]\& ${\it dis}$(${\it loc}$,$x$) = isl($f$)
\\[0ex]\& (($\uparrow$can{-}apply(${\it afr}$(${\it loc}$);${\it knd}$)) $\Rightarrow$ ($x$ $\in$ do{-}apply(${\it afr}$(${\it loc}$);${\it knd}$)))
\\[0ex]Rsends(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$)=$>$ ${\it cl}$(source($l$),$<$5, ${\it knd}$, $l$$>$) = Rsends(${\it ds}$;${\it knd}$;$T$;$l$;${\it dt}$;$g$)
\\[0ex]\& (\=($\uparrow$isrcv(${\it knd}$))\+
\\[0ex]$\Rightarrow$ \=((($\uparrow$lnk(${\it knd}$) = $l$) $\Rightarrow$ ($T$ = ${\it dt}$(tag(${\it knd}$))?Void))\+
\\[0ex]\& destination(lnk(${\it knd}$)) = source($l$)))
\-\-\\[0ex]\& $\forall$$z$$\in$dom(${\it ds}$). $A$=${\it ds}$($z$) $\Rightarrow$  ((${\it sv}$($z$)).1) = $A$
\\[0ex]\& ${\it av}$(${\it knd}$) = $T$
\\[0ex]\& $\forall$$k$$\in$dom(lnk{-}decl($l$;${\it dt}$)). $A$=lnk{-}decl($l$;${\it dt}$)($k$) $\Rightarrow$  ${\it av}$($k$) = $A$
\\[0ex]\& Normal(${\it dt}$)
\\[0ex]\& ($\forall$${\it tg}$$\in$map($\lambda$$p$.$p$.1;$g$). (${\it knd}$ $\in$ ${\it sfr}$($l$,${\it tg}$)))
\\[0ex]\& ($\forall$$z$$\in$fpf{-}domain(${\it ds}$). (${\it knd}$ $\in$ ${\it rfr}$(source($l$),$z$)))
\\[0ex]\& (($\uparrow$can{-}apply(${\it bfr}$(source($l$));${\it knd}$)) $\Rightarrow$ ($l$ $\in$ do{-}apply(${\it bfr}$(source($l$));${\it knd}$)))
\\[0ex]Rpre(${\it loc}$,${\it ds}$,$a$,$p$,$P$)=$>$ ${\it cl}$(${\it loc}$,$<$6, $a$$>$) = Rpre(${\it loc}$;${\it ds}$;$a$;$p$;$P$)
\\[0ex]\& $\forall$$z$$\in$dom(${\it ds}$). $A$=${\it ds}$($z$) $\Rightarrow$  ((${\it sv}$($z$)).1) = $A$
\\[0ex]\& ${\it av}$(locl($a$)) = Outcome
\\[0ex]\& ($\forall$$z$$\in$fpf{-}domain(${\it ds}$). (locl($a$) $\in$ ${\it rfr}$(${\it loc}$,$z$)))
\\[0ex]Rkframe(${\it loc}$,$k$,$L$)=$>$ ${\it cl}$(${\it loc}$,$<$7, $k$$>$) = Raframe(${\it loc}$;$k$;$L$) \& ${\it afr}$(${\it loc}$,$k$) = (inl $L$ )
\\[0ex]Rksframe(${\it loc}$,$k$,$L$)=$>$ ${\it cl}$(${\it loc}$,$<$8, $k$$>$) = Rbframe(${\it loc}$;$k$;$L$) \& ${\it bfr}$(${\it loc}$,$k$) = (inl $L$ )
\\[0ex]Rrframe(${\it loc}$,$x$,$L$)=$>$ ${\it cl}$(${\it loc}$,$<$9, $x$$>$) = Rrframe(${\it loc}$;$x$;$L$) \& ${\it rfr}$(${\it loc}$,$x$) = $L$
\-
\end{tabbing}